ModuleArityMismatch.agda:8,2-19
The arguments to M do not fit the telescope (A₁ : Set)
when checking the module application module M′ = M A A
